I have now proven the duality theorem for directed graphs (analogous to type duality), which is the toy-result of what I'm really after for globular types.

I still find it very frustrating that pre-commit produces such a mess on commented code :(

Unfortunately, it is a choice between two evils, unless we want to start playing with making changes to the auto-formatter. Luckily your issue can be avoided by being mindful of how one comments code.

Your best course of action here is to look through the commit history for a point in time where the code wasn't jumbled. Alternatively, you could try something like text replacing -- with \n, but then you will have to manually indent things again after.

Hiya! It looks like this PR is perhaps growing a bit outside the scope of the original goal. While I don't doubt the changes are relevant to one another, do you think it perhaps would be possible to split it up into some more manageable chunks for the eventual review?

Oh, I see this PR is marked as ready for review. What's the status here?

It's ready for review. The contents of this PR are such that it can be merged to the library (modulo review comments, of course).

On the other hand, I haven't split it up yet, because if it is going to take a while for this to be reviewed then I prefer to keep working on it until I got all the HS-universes and all the corresponding duality theorems.

I see, okay, so do you want a heads-up about when I think I'll be able to review?

Sure, or alternatively perhaps you can review the graph theory here in this PR and then I can separate it out into a separate PR when I resolved your comments.

okay, sounds good

One thing I'm still debating on with myself is whether I should use the terminology "displayed" or "dependent".

Displayed is such a weird word to use in this context, but on the other hand it is the standard for some people.

I used the word "displayed" when I defined reflexive graphs because I had my eye toward wild categories, but I agree the landscape is pretty different for graphs. At the end of the day it's your domain though, so it's up to you what you want to call it.

Amazing effort!

This review regards modules in foundation-core, foundation, and graph-theory.

Thanks for the swift review Fredrik!

That was a very helpful review, Fredrik! I have also made the corresponding changes for globular types, so that you don't have to make the same remarks again.

Thanks so much!

I'm glad! 😄